Nuprl Definition : d-machine
0,22
postcript
pdf
d-machine(
i
;
M
;
dec
)
== <
dec
==
,(
k
,
v
,
s
,
x
. if islocal(
k
)
destination(lnk(
k
)) =
i
M
.ef(
k
,
x
,
s
,
v
)?
s
(
x
) else
s
(
x
) fi)
==
,(
k
,
v
,
s
. if islocal(
k
)
destination(lnk(
k
)) =
i
filter(
m
.source(mlnk(
m
)) =
i
;
M
.sends(
k
,
s
,
v
))
== ,(
k
,
v
,
s
.
else nil fi)>
latex
Definitions
<
a
,
b
>
,
M
.ef(
k
,
x
,
s
,
v
)?
w
,
f
(
a
)
,
if
b
t
else
f
fi
,
p
q
,
islocal(
k
)
,
destination(
l
)
,
lnk(
k
)
,
filter(
P
;
l
)
,
x
.
A
(
x
)
,
a
=
b
,
source(
l
)
,
mlnk(
m
)
,
M
.sends(
k
,
s
,
v
)
,
nil
FDL editor aliases
d-machine
origin